es:ES, T:Type, X:MaInterface(T), i:Id.
(i  dom(X))  (ma-interface-consistent-at(es;i;X)  ) 

latex

Definitions

{x:A| B(x)} , Knd, b, Top, left + right, x:AB(x), x:A. B(x), State(ds), Type, x:A  B(x), hasloc(k;i), x. t(x), a:A fp B(a), x.A(x), IdDeq, x  dom(f), P  Q, ES, ma-interface-consistent-at(es;i;X), MaInterface(T), Id, , t  T, strong-subtype(A;B), EqDecider(T), KindDeq, Atom$n, if b then t else f fi , s = t, f(x)?z, vartype(i;x), loc(e), E, f(x), t.1, valtype(e), kind(e), e@i. P(e), P & Q, let x,y = A in B(x;y)

Lemmas

alle-at wf, es-kind wf, es-valtype wf, pi1 wf, fpf-ap wf, es-E wf, es-loc wf, subtype rel wf, es-vartype wf, fpf-cap wf, Kind-deq wf, strong-subtype-deq-subtype, strong-subtype-set3, strong-subtype-self, event system wf, Id wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf